﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace CNFProblem.CNF
{
    class Algo176 : IAlgorithm
    {
        private static List<int> getPureSymbols(LogicalFormula3CNF formula, out List<int> antiPure)
        {
            List<int> notUsed = formula.Variables.Select(v => v.Id).ToList();
            List<int> pure = new List<int>();
            antiPure = new List<int>();
            foreach(LiteralAlternative la in formula)
            {
                for (int i = 0; i < la.GetLenght(); i++)
                {
                    int id = la.GetId(i);
                    if (!la.GetNeg(i))
                    {
                        if (notUsed.Contains(id)) //it may be pure
                        {
                            notUsed.Remove(id);
                            pure.Add(id);
                        }
                        else if (antiPure.Contains(id)) //it is for sure not antipure (nor antipure)
                        {
                            antiPure.Remove(id);
                        }
                    }
                    else
                    {
                        if (notUsed.Contains(id)) //it may be antipure
                        {
                            notUsed.Remove(id);
                            antiPure.Add(id);
                        }
                        else if (pure.Contains(id)) // it is for sure not antipure (nor pure)
                        {
                            pure.Remove(id);
                        }
                    }
                }
            }
            return pure;
        }

        private bool TrimPureSymbols(ref LogicalFormula3CNF formula, ref Dictionary<int, bool> constrains, ref Dictionary<int, bool> values)
        {
            List<int> AntiPureSymbols;
            List<int> PureSymbols = getPureSymbols(formula, out AntiPureSymbols);
            int removed = 0;
            foreach (int id in PureSymbols)
            {
                values[id] = true;
                if (!constrains.ContainsKey(id)) constrains.Add(id, true);
                else throw new ConstraintViolationException();
                removed += formula.RemoveAll(l => l.HasId(id));
            }
            foreach (int id in AntiPureSymbols)
            {
                values[id] = false;
                if (!constrains.ContainsKey(id)) constrains.Add(id, false);
                else throw new ConstraintViolationException();
                removed += formula.RemoveAll(l => l.HasId(id));
            }
            if (removed > 0) return true;
            return false;
        }

        private bool ComputeRecursive(LogicalFormula3CNF formula, Dictionary<int,bool> SetUpSymbols, ref Dictionary<int, bool> values)
        {
            foreach (KeyValuePair<int, bool> symbol in SetUpSymbols)
            {
                //constrains are violated
                if (values[symbol.Key] != symbol.Value) return false;
            }
            if (formula.Count == 0) 
                return true;
            try
            {
                if (TrimPureSymbols(ref formula, ref SetUpSymbols, ref values))
                    return ComputeRecursive(formula, SetUpSymbols, ref values);
            }
            catch (ConstraintViolationException e)
            {
                return false;
            }
            //la1 = x, y, z
            LiteralAlternative la1 = formula.First();
            
            //Alternative which has the same symbol as the first symbol of la1 but with diffrent sign
            LiteralAlternative la2 = formula.Where(la => la.HasId(la1.GetId(0)) && (la.IsIdNotNegated(la1.GetId(0)) == la1.GetNeg(0) || la.IsIdNegated(la1.GetId(0)) != la1.GetNeg(0))).First();
            formula.Remove(la1);
            formula.Remove(la2);

            //la2 = !x, u, v
            la2.MadeIdFirst(la1.GetId(0));

            //formula now is f'
            //f' && la1 && la2 == old formula

            VariableValue x = new VariableValue(la1.GetId(0),!la1.GetNeg(0));
            VariableValue y = la1.GetLenght() > 1 ? new VariableValue(la1.GetId(1),!la1.GetNeg(1)) : x; //for easier code if there is no such symbol we treat it as already exsisting one ( x || x == x )
            VariableValue z = la1.GetLenght() > 2 ? new VariableValue(la1.GetId(2),!la1.GetNeg(2)) : x;
            VariableValue u = la2.GetLenght() > 1 ? new VariableValue(la2.GetId(1), !la2.GetNeg(1)) : new VariableValue(x.id, !x.value);
            VariableValue v = la2.GetLenght() > 2 ? new VariableValue(la2.GetId(2), !la2.GetNeg(2)) : new VariableValue(x.id, !x.value);

            //f' | xu
            //Here we are checking if x & u does not violate constraints
            if ((!SetUpSymbols.ContainsKey(x.id) || SetUpSymbols[x.id] == x.value) 
                && (!SetUpSymbols.ContainsKey(u.id) || SetUpSymbols[u.id] == u.value))
            {
                Dictionary<int, bool> newSetUp = new Dictionary<int, bool>(SetUpSymbols);
                if (!newSetUp.ContainsKey(x.id)) newSetUp.Add(x.id, x.value);
                if (!newSetUp.ContainsKey(u.id)) newSetUp.Add(u.id, u.value);
                Dictionary<int, bool> newValues = new Dictionary<int, bool>(values);
                newValues[x.id] = x.value;
                newValues[u.id] = u.value;
                if (ComputeRecursive(formula, newSetUp, ref newValues))
                {
                    values = newValues;
                    return true;
                }
            }

            //f' | x!uv
            if ((!SetUpSymbols.ContainsKey(x.id) || SetUpSymbols[x.id] == x.value) 
                && (!SetUpSymbols.ContainsKey(u.id) || SetUpSymbols[u.id] == !u.value)
                && (!SetUpSymbols.ContainsKey(v.id) || SetUpSymbols[v.id] == v.value)
                )
            {
                Dictionary<int, bool> newSetUp = new Dictionary<int, bool>(SetUpSymbols);
                if (!newSetUp.ContainsKey(x.id)) newSetUp.Add(x.id, x.value);
                if (!newSetUp.ContainsKey(u.id)) newSetUp.Add(u.id, !u.value);
                if (!newSetUp.ContainsKey(v.id)) newSetUp.Add(v.id, v.value);
                Dictionary<int, bool> newValues = new Dictionary<int, bool>(values);
                newValues[x.id] = x.value;
                newValues[u.id] = !u.value;
                newValues[v.id] = v.value;
                if (ComputeRecursive(formula, newSetUp, ref newValues))
                {
                    values = newValues;
                    return true;
                }
            }

            //f' | !xy
            if ((!SetUpSymbols.ContainsKey(x.id) || SetUpSymbols[x.id] == !x.value)
                && (!SetUpSymbols.ContainsKey(y.id) || SetUpSymbols[y.id] == y.value))
            {
                Dictionary<int, bool> newSetUp = new Dictionary<int, bool>(SetUpSymbols);
                if (!newSetUp.ContainsKey(x.id)) newSetUp.Add(x.id, !x.value);
                if (!newSetUp.ContainsKey(y.id)) newSetUp.Add(y.id, y.value);
                Dictionary<int, bool> newValues = new Dictionary<int, bool>(values);
                newValues[x.id] = !x.value;
                newValues[y.id] = y.value;
                if (ComputeRecursive(formula, newSetUp, ref newValues))
                {
                    values = newValues;
                    return true;
                }
            }

            //f' | !x!yz
            if ((!SetUpSymbols.ContainsKey(x.id) || SetUpSymbols[x.id] == !x.value)
                && (!SetUpSymbols.ContainsKey(y.id) || SetUpSymbols[y.id] == !y.value)
                && (!SetUpSymbols.ContainsKey(z.id) || SetUpSymbols[z.id] == z.value)
                )
            {
                Dictionary<int, bool> newSetUp = new Dictionary<int, bool>(SetUpSymbols);
                if (!newSetUp.ContainsKey(x.id)) newSetUp.Add(x.id, !x.value);
                if (!newSetUp.ContainsKey(y.id)) newSetUp.Add(y.id, !y.value);
                if (!newSetUp.ContainsKey(z.id)) newSetUp.Add(z.id, z.value);
                Dictionary<int, bool> newValues = new Dictionary<int, bool>(values);
                newValues[x.id] = !x.value;
                newValues[y.id] = !y.value;
                newValues[z.id] = z.value;
                if (ComputeRecursive(formula, newSetUp, ref newValues))
                {
                    values = newValues;
                    return true;
                }
            }
            return false;
        }

        public bool Compute(LogicalFormula3CNF formula, out Dictionary<int, bool> values)
        {
            values = formula.Variables.GetAsFalse();
            return ComputeRecursive(formula, new Dictionary<int,bool>(), ref values);
        }
    }
}
